[#15064] feat: rewrite the Verso docstring parser to produce accurate syntax - #58

Verso carried its own copy of the docstring parser, producing the same syntax under the same node kinds. It now calls `Lean.Doc.Parser`, which takes `Verso/Parser.lean` from 1003 lines to 343; what stays is the generic combinator prelude that Verso and the reference manual use for lexers of their own.

The elaboration interfaces take views rather than syntax. `InlineExpander`, `BlockExpander` and `PartCommand` receive an `InlineView` or `BlockView`, and `elabInline`, `elabBlock` and `partCommand` build it once and pass it to each expander. The registry stays keyed on syntax kind, so a package can still replace an element's expander. Views carry a production's delimiters and arguments with their positions, which is what a code action needs to write a replacement.

`VersoLiteral` abstracts the kinds whose tokens denote a string: `decode` reads the text and `encode` writes a token at a given position. String literals and Verso's seven content tokens instantiate it, so a parser or a diff takes one argument again rather than a location and a string.

Verso's linters read the syntax a document is made of, so the typography and header-tag linters move to views along with everything else that matched on it.

The parser reports two mistakes that its predecessor recovered from silently. A `#doc` in `Tests/VersoBlog.lean` ran to the end of the file and swallowed two `#docs`, four `#guard`s, and a test appended later; those documents get delimiters, the missing `#guard_msgs` returns, and the deprecation test uses the role it asserts a warning for. `#.` opened a section that rendered as a paragraph.

Folding ranges now cover the lists inside a document body, so two expectations gain entries.

The views, the content tokens and the literal class are named through `open`, so a signature reads `TSyntaxArray ``inline` rather than spelling out a namespace. Each file opens the names it uses: `Lean.Doc` as a whole brings in the document types, whose `Inline` and `Block` collide with Verso's own inside a quotation.

A view is destructured by field, so a pattern says which part of an element it takes.

The remaining full names are the ones that resolution does not reach: an `inline_to_string` key, which the attribute reads literally, and the syntax kinds a linter compares against, which are `Name` literals.

`Verso.Parser` no longer re-exports the productions it used to define, which named the same things as `Lean.Doc.Parser` and shadowed them.

Every element that Verso reads is read through a view: the language server's delimiter pairing, directive resizing and semantic tokens, and the roles that reach for their own syntax. `Lean.Doc.Syntax` is gone from Verso, including the `open` that `#doc` used to add to a document's scope.

`warnLongLines` takes a code block and measures each line token, which the parser has already separated, rather than recovering the lines from the file. Its note and hint are built only for a line that is too long. A test covers the limit, a line that exceeds it, and the option that turns it off.

`DocDef.defSite` is the name it defines.

The rewritten parser reports the position where a construct opened rather than the end of input, and
names the delimiter it expects.

…rewrite

The expanders read views, and the long-line warning moves to the code block expander that renders
wide enough for it to matter.